i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
a:((k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)T)), upd:update-spec(ds;da).
x  dom(ds)  update-spec-decl(upd;ds)  ecl-machine2(i;ds;da;x;T;ks;a;upd)  Realizer 

latex

Definitions

Type, f || g, f(x), Knd, (x  l), {x:A| B(x) }, x:AB(x), <a,b>, nil, f(x)?z, A/x,y. B(x;y), list_accum(x,a.f(x;a);y;l), t  T, x:A. B(x), x.A(x), x. t(x), x : v, f  g, State(ds), x:AB(x), Valtype(da;k), P  Q, R-state-var(i;ds;da;x;T;ks;tr), update-spec-decl(upd;ds), Atom$n, x:A. B(x), Realizer, update-spec-vars(upd), xL.R(x), ecl-machine2(i;ds;da;x;T;ks;a;upd), a:A fp B(a), type List, , , update-spec(ds;da), Top, A, IdDeq, x  dom(f), b, Id, False, b, s = t, Prop, AB, , P & Q, P  Q, Unit, left+right, 2of(t), Void, f(a), 1of(t), if b t else f fi, x:A. B(x), KindDeq, product-deq(A;B;a;b), x,y. t(x;y), EqDecider(T), S  T, P  Q, a = b, s ~ t, SQType(T), {T}

Lemmas

Id sq, assert-eq-id, fpf-compatible-singles, fpf-compatible-single-iff, fpf-compatible-single, fpf-compatible-symmetry, fpf-compatible-join2, list accum wf, product-deq wf, Kind-deq wf, ifthenelse wf, fpf-join-cap-sq, fpf-cap-single, eqof eq btrue, pi1 wf, pi2 wf, subtype rel dep function, fpf-cap wf, top wf, fpf-cap-join-subtype, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, subtype rel self, bnot wf, update-spec-decl wf, not wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, update-spec wf, nat wf, bool wf, fpf wf, Rall wf, update-spec-vars wf, R-state-var wf, fpf-ap wf, ma-valtype wf, decl-state wf, fpf-join wf, fpf-single wf, Id wf, id-deq wf, l member wf, Knd wf